$a$ = $b$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$eqof(IdLnkDeq)($a$,$b$)